Nuprl Lemma : fpf-single_wf3
11,40
postcript
pdf
A
,
B
:Type,
x
:
A
. fpf-single(
x
;
B
)
fpf(
A
;
a
.Type)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
{
x
:
A
|
B
(
x
)}
,
Type
,
x
:
A
B
(
x
)
,
x
.
A
(
x
)
,
type
List
,
[]
,
cons(
car
;
cdr
)
,
<
a
,
b
>
,
fpf-single(
x
;
v
)
,
fpf(
A
;
a
.
B
(
a
))
Lemmas
l
member
wf
origin
A,B:Type, x:A. fpf-single(x; B) 
fpf(A; a.Type) A,B:Type, x:A. fpf-single(x; B) fpf(A; a.Type) Tx:A. B(x) l)
B(x)
x.A(x)